Designing and fabricating electronic devices typically involves many steps, known as a “design flow.” The particular steps of a design flow often are dependent upon the type of circuitry, its complexity, the design team, and the device fabricator or foundry that will manufacture the electronic device. Several steps are common to most design flows for electronic devices. Initially, a specification for a new circuit is transformed into a logical design, sometimes referred to as a register transfer level (RTL) description of the circuit. With this logical design, the circuit can be described in terms of both the exchange of signals between hardware registers and the logical operations that can be performed on those signals. The logical design typically employs a Hardware Design Language (HDL), such as Verilog, Very high speed integrated circuit Hardware Design Language (VHDL), or the like.
At various stages of the design flow, the design is transformed into a different representation, for example, the transformation of the design from an RTL representation to a gate-level netlist representation during synthesis, the transformation of the gate-level netlist to a physical design layout, or the like. These transformations are intended to convert the design into an equivalent representation, albeit at a different level of abstraction than the previous representation of the design, which retains the functionality of the design. To help ensure that a transformation did not alter the functionality of the design, an equivalence of the different design representations can be determined, for example, using a logical equivalence tool that often include one or more formal techniques, such as a Binary Decision Diagram (BDD), a Boolean Satisfiability (SAT) Solver, an Automatic Test Pattern Generator (ATPG), Cut Point Prover, or the like.
While the use of the logical equivalence tool can be an effective way to determine logical equivalence between multiple designs at different levels of abstraction, it often takes a non-insignificant amount of time to load the multiple designs into the logical equivalence tool. Typically, the logical equivalence tool will parse the entirety of each design, identify which portions of each design correlate to each other, and link those correlated portions together in a data structure. After the data structure has been built, the logical equivalence tool can attempt to determine logical equivalence between the correlated portions based on the data structure.
Oftentimes, designers wish to utilize the logical equivalence tools to check only a subset of the designs for logical equivalence, but these logical equivalence tools still have to perform the time-consuming operation of loading the entirety of each design before checking the subset of the designs. Some synthesis tools have attempted to truncate this initial loading burden by generating one or more additional design files that include portions of the designs that the logical equivalence tools wish to check for logical equivalence. The logical equivalence tools can then load the entirety of these newly generated design files and check them for equivalence. The assumption, however, that an equivalence between the newly generated design files necessarily renders equivalent the portions of the designs included in the newly generated design files can be fallacious, as the generation of the design files is often susceptible to errors. In other words, when a conventional logical equivalence tool wishes to check only a subset of multiple designs, there is a tradeoff between load time and accuracy.